sig Name {}

sig Address{}


sig AddressBook {
	names: set Name,
	addr: names -> Address
}

pred addAddress(b,b': AddressBook, n:Name, a:Address){
	b'.names = b.names + n and
	b'.addr = b.addr ++ (n->a)
}

fact domAddrIsNames{
	all b: AddressBook | b.addr.Address  = b.names
}

fact addIsFunctional{
	all b:AddressBook | all n: b.names | one n.(b.addr)
}

assert addAddrChangesAddressBook{
	all b,b': AddressBook | all n:Name | all a:Address | addAddress[b, b', n, a]  => b!=b'
}


run addAddress
